p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))).
rv-iid(p;n.f(n);n.X(n))
 (mean:.
 (E(f(0);X(0)) = mean)
  nullset(p;s.q:
  nullset(p;s.(0 < q
  nullset(p;s.& (n:. m:. ((n < m) & q  |0  i < m. (1/m) * (X(i)(s)) - mean|))))) 

latex

Definitions

x:A. B(x), , x(s), P  Q, P & Q, t  T, x. t(x), P  Q, P  Q, T, True, , A  B, A, False, x:A. B(x), Top, S  T, A c B, t  ...$L, suptype(S; T), Outcome, {i..j}, , a  b  T , i  j < k, X + Y, rv-const(a), r * s, r - s, if b then t else f fi , tt, FinProbSpace, RandomVariable(p;n)

Lemmas

slln-lemma4, rv-add wf, rv-const wf, qmul wf, int inc rationals, rv-iid-add-const, expectation-rv-add, qadd wf, squash wf, true wf, rationals wf, expectation-rv-const, expectation wf, le wf, rv-iid wf, nat wf, random-variable wf, finite-prob-space wf, qinverse q, nullset-monotone, top wf, qless wf, qle wf, qabs wf, qsum wf, qdiv wf, nat properties, int-eq-in-rationals, int-rational, int seg wf, p-outcome wf, int nzero-rational, nequal wf, subtype rel function, length wf nat, false wf, qsub wf, sum plus q, prod sum l q, qsum-const, qmul over plus qrng, qmul over minus qrng, qmul comm qrng, qmul ac 1 qrng, qmul-qdiv-cancel4, qmul assoc